r:Rng, a, b:.
(a  b)
 (E, F:({a..b}|r|).
 ((r) a  i < b. E(i) +r F(i)) = (((r) a  i < b. E(i)) +r ((r) a  i < b. F(i)))  |r|) 

latex

Definitions	IMonoid, t  T, IAbMonoid, x:A. B(x), t.2, t.1, , P & Q, Mon, Group{i}, AbGrp, r+gp, *, |g|, (r) i  k < j. E(k)
Lemmas	rng wf, abgrp wf, comm wf, grp id wf, grp op wf, grp car wf, monoid p wf, add grp of rng wf b, mon itop op